『Chapar: Certified Causally Consistent Distributed Key-Value Stores』
#論文 #未読
あだむっち先生のとこの論文。POPL'16。もちろん Coq
概要
いまのネットサービスはノードのクラッシュとかネットワークの分断とか起きても生きていないといけないよね
因果一貫性 causal consistency は、このようなサービスに要求される強めの一貫性の一つだよ
一貫性を持つ KVS とかね
Chaper というフレームワークを作ったよ
因果一貫性の検証
複製可能なKVS実装とそのクライアントの検証のため
KVSの実装とそのクライアントが正しい実装である条件を形式化したよ
因果一貫性に関する (斬新な) 操作的意味論を作ったよ
(斬新な) 証明テクニックを使って、2つのKVS実装の因果一貫性を証明したよ
2つ、というのは、KVSの実装2つなのか、サーバとクライアントの2つなのか、わからない
シンプルな自動モデル検査器も作ったよ
クライアント用
独立してサーバとクライアントの検証をしたので、これらの実装は正しいことが言えるよ
フレームワークは Coq で作って OCaml に抽出してビルドして実行できるようになってるよ